the_es:event_system{i:l}, e:es-E(the_es).
before(e)  ({e':es-E(the_es)| loc(e') = loc(e)  Id}  List) 

latex

Definitions	x:A. B(x), t  T, before(e), P  Q, T, True, prop{i:l}, Y, if b then t else f fi , tt, ff, ge(i; j), A  B, A, False, , SWellFounded(R(x;y)), x:A. B(x), , Unit, P  Q, P  Q,
Lemmas	es-locl-swellfnd, nat wf, es-E wf, event system wf, le wf, es-locl wf, es-first wf, bool wf, eqtt to assert, Id wf, es-loc wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, append wf, nat properties, ge wf, es-pred wf, es-pred-locl, subtype rel list, es-loc-pred